  Natural
→ ∀(natural : Type)
→ ∀(succ : natural → natural)
→ ∀(zero : natural)
→ natural
